(0) Obligation:

Clauses:

factorial1(N, F) :- ','(>(N, 0), ','(is(N1, -(N, 1)), ','(factorial1(N1, F1), is(F, *(N, F1))))).
factorial1(0, 1).
factorial2(N, F) :- factorial2(0, N, 1, F).
factorial2(I, N, T, F) :- ','(<(I, N), ','(is(I1, +(I, 1)), ','(is(T1, *(T, I1)), factorial2(I1, N, T1, F)))).
factorial2(N, N, F, F).
factorial3(N, F) :- factorial3(N, 1, F).
factorial3(N, T, F) :- ','(>(N, 0), ','(is(T1, *(T, N)), ','(is(N1, -(N, 1)), factorial3(N1, T1, F)))).
factorial3(0, F, F).

Query: factorial(g,a)

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph ICLP10.

(2) TRUE